P:(Unit). Dec(P())  Dec(x:Unit. P(x)) 

latex

Definitions	x:A. B(x), , P  Q, x(s), t  T, x. t(x), finite-type(T), x:A. B(x), , A  B, A, False, Surj(A;B;f), {i..j}, i  j < k, P & Q, Unit,
Lemmas	decidable-exists-finite, unit wf, decidable wf, it wf, le wf, int seg wf, surject wf